FDL - Nuprl Lemma : l_disjoint

Nuprl Lemma : l_disjoint_intersection2

11,40

T:Type, eq:EqDecider(T), a, b, c:(T List).
(l_disjoint(T;a;b)

l_disjoint(T;a;c))

l_disjoint(T;a;l_intersection(eq;b;c))

Definitions l_disjoint(T;l1;l2), P Q, x:AB(x), P Q, P Q, x:A. B(x), x:A B(x), P & Q, P Q, left + right, type List, EqDecider(T), Type, t T

Lemmas l disjoint intersection, or functionality wrt iff, l disjoint-symmetry

Definitions	l_disjoint(T;l1;l2), P Q, x:AB(x), P Q, P Q, x:A. B(x), x:A B(x), P & Q, P Q, left + right, type List, EqDecider(T), Type, t T
Lemmas	l disjoint intersection, or functionality wrt iff, l disjoint-symmetry